T, V:Type, A, B:(T), f:({x:T| (A(x))} V), g:({x:T| (B(x))} V).
(x.if A(x) then f(x) else g(x) fi ) = [x.(A(x))? f : g]  {x:T| ((A(x)))  ((B(x)))} V 

latex

Definitions	Type, t  T, , x:AB(x), f(a), x:A. B(x), b, {x:A| B(x)} , x.A(x), <a, b>, left + right, s = t, P  Q, [P? f : g], if b then t else f fi , False, A, Unit, case b of inl(x) => s(x) | inr(y) => t(y), True, x:A.B(x), x. t(x), if p:P then A(p) else B fi , Void, P  Q, bool-decider(b), , b, x:A  B(x), P & Q, P  Q, Top, Dec(P)
Lemmas	decidable wf, decidable or, decidable assert, branch-ifthenelse, ifthenelse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, bool-decider wf, not wf, branch wf2, true wf, false wf, assert wf, bool wf